package verificateur;
import instruction.Affectation;

import java.io.IOException;
import java.util.LinkedList;

import structureDonnee.Block;
import structureDonnee.Expression;
import structureDonnee.Inequalite;
import structureDonnee.Invariant;
import structureDonnee.Node;

import math.Fraction;


public class Verificateur0 {
	final static int CANONIQUE = 1;
	
	public Verificateur0(){}

	//alogrithm fourrier Motzkin pour calculer la Post-Condition apres une affectation
	public Invariant postCondition(Invariant inv, 
									Affectation aff, 
									EnsembleVariable ev){
		int n = ev.size();
		//chercher le nom de variable de v dans l'Affectation
		int index=0;
		while(!aff.getVariable().getNom().equals(ev.listeVariable.get(index).getNom())){
			index++;
			if(index==n) System.out.println("AffectationToVariableUnknown");
		}		
		LinkedList<Inequalite> listIneNew = new LinkedList<Inequalite>();
		Fraction aj=aff.getExpr().getListExpr().get(index);//aj est le coefficient de variable v
		//aj cas de inversible
		if(!aj.equals(0)){//aj!=0
			//pour chaque ine
			for(Inequalite ine : inv.listIne){
				LinkedList<Fraction> listtmp = new LinkedList<Fraction>();
				for (int i = 0; i < n; i++){
					if(i!=index){
						//calcule nouveau a(i) i!=j
						Fraction aai = ine.getExpr().getListExpr().get(i).minus(ine.getExpr().getListExpr().get(index).dividedBy(aj).times(aff.getExpr().getListExpr().get(i)));
						listtmp.add(i, aai);
					}
					else{
						//calcule nouveua a(j)
						Fraction aaj = ine.getExpr().getListExpr().get(index).dividedBy(aj);
						listtmp.add(index, aaj);
					}
				}
				//calculte constant
				Fraction dd = ine.getExpr().getListExpr().get(n).minus(ine.getExpr().getListExpr().get(index).dividedBy(aj));//constant
				listtmp.add(n, dd);

				Inequalite ineNew = new Inequalite(new Expression(listtmp));
				listIneNew.add(ineNew);
			}
			return new Invariant(listIneNew);
		}

		//aj cas de non-inversible, aj==0
		else{
			LinkedList<Inequalite> listIneNewPos = new LinkedList<Inequalite>();
			LinkedList<Inequalite> listIneNewNeg = new LinkedList<Inequalite>();
			
			for(Inequalite ine : inv.listIne){
				Fraction ajj=ine.getExpr().getListExpr().get(index);
				//inequelite de type III
				if(ajj.equals(0)){
					 listIneNew.add(ine);
				}
				else{
					//inequalite de type I
					if (ajj.compareTo(0)==1){
						LinkedList<Fraction> dl= new LinkedList<Fraction>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, ine.getExpr().getListExpr().get(i).dividedBy(ajj).times(-1));
							}
							else{
								dl.add(index,new Fraction(0));
							}
						}
						//ajouter constant
						dl.add(n, ine.getExpr().getListExpr().get(n).dividedBy(ajj).times(-1));
						listIneNewPos.add(new Inequalite(new Expression(dl)));
					}
					//inequelite de type II
					if (ajj.compareTo(0)==-1){
						LinkedList<Fraction> dl= new LinkedList<Fraction>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, ine.getExpr().getListExpr().get(i).dividedBy(ajj).times(-1));
							}
							else{
								dl.add(index,new Fraction(0));
							}
						}
						//ajouter constant
						dl.add(n, ine.getExpr().getListExpr().get(n).dividedBy(ajj).times(-1));
						listIneNewNeg.add(new Inequalite(new Expression(dl)));
					}
				} 
			}
			//lier des inePos et des ineNeg pour creer des nouvelles liste de ine
			for (Inequalite inePos:listIneNewPos){
				for (Inequalite ineNeg:listIneNewNeg){
					LinkedList<Fraction> dll = new LinkedList<Fraction>();
					for(int i = 0; i< n+1; i++){
						Fraction tmp = ineNeg.getExpr().getListExpr().get(i).minus(inePos.getExpr().getListExpr().get(i));
						dll.add(i, tmp);
					}
					Inequalite ineNew = new Inequalite(new Expression(dll));
					listIneNew.add(ineNew);
				}
			}
			//ajouter j =aff equivalent au (j>=aff j<=aff)
			Inequalite ineNew1 = new Inequalite(aff.getExpr());
			ineNew1.getExpr().getListExpr().add(index, new Fraction(-1));
			ineNew1.getExpr().getListExpr().add(n, aff.getExpr().getListExpr().get(n));

			Inequalite ineNew2 = new Inequalite();
			for(Fraction f:ineNew1.getExpr().getListExpr())
				ineNew2.getExpr().getListExpr().add(f.negative());
			
			listIneNew.add(ineNew1);
			listIneNew.add(ineNew2);
			//
			return new Invariant(listIneNew);
		}
	}

	//utiliser Algorithm Simplex pour simplifier Invariant calculer par PostCondition
	//pour chaque inequalite dans Invariant, on prend les restes Inequalites dans cette invariant comme environement
	//si cette inequalite est toujours vrai, on peut le supprimer, sinon, il peut rester
	public Invariant simplifierPostCondition(Invariant inv){
		Invariant newInv = inv;
		for (Inequalite ine : newInv.listIne){
			if(newInv.listIne.size()==1) return newInv;//si il reste qu un inequalite dans invariant, return
			else{
				newInv.listIne.remove(ine);
				TransformToSimplex tts = new TransformToSimplex(newInv,ine, CANONIQUE);
				if( (tts.value()>=0) & (tts.verifierStrict()) ){//cette ine peux etre supprime
					continue;//rien faire, continue boucle
				}
				else{//cette ine ne doit pas etre supprime, on le rajouter dans Invariant
					newInv.listIne.add(ine);
				}
			}
		}
		return newInv;
	}
	
	//verifier un node, un Invariant. Inv.mEnviron => Inv.invariant
	public boolean verifierNode(Node node, EnsembleVariable ev){
		//on utilise class simplex pour verifier implication.
//		Simplex sim = new Simplex();
//		boolean YesNo = sim.verifierImplication(node.getEnviron(), node.getInvariant());
	
		//pour integrer Simplexe. utiliser class simplex pour verifier implication
//		/*
		boolean YesNo = true;
		if(node.getEnviron().listIne.isEmpty()) YesNo = true;
		else{
			for (Inequalite mIne: node.getInvariant().getListIne() ){
				TransformToSimplex ts = new TransformToSimplex(node.getEnviron(),mIne,CANONIQUE);
	//			YesNo = YesNo & (ts.value()>=0);
				if(mIne.getStrict()) YesNo = YesNo & (ts.value()>0) & (ts.verifierStrict());
				else YesNo = YesNo & (ts.value()>=0) & (ts.verifierStrict());
			}
		}		 
//		 */
		
	//	if(YesNo) System.out.println("verifierNODE");	
	//	if(!YesNo) {System.out.println("Node WRONG!");return false;}

		if(node.getInstr().getType() == 0 ){ //instruction is affectation, executer aff
			if(!node.getSuivants().isEmpty()){
	//			executerAffectation(node,ev);
				Invariant tmpInv = postCondition(node.getInvariant(),node.getInstr(),ev);
//				Invariant tmpInv = simplifierPostCondition( postCondition(node.getInvariant(),node.getInstr(),ev) );
				node.suivants.getFirst().environ = new Invariant();
				node.suivants.getFirst().environ.listIne.addAll(tmpInv.listIne);
				System.out.println("executerAffecatation");	
			}
			else System.out.println("Wrong!NodeFinDeArbreAvecAffectation");
		}

		if(node.instr.getType() == 1){//instruction FaireRien
			if(node.suivants == null){
				System.out.println("fin de arbre");
			}
			else{
				if(!node.suivants.isEmpty()){}
				else System.out.println("fin de arbre");
			}
		}
		if(node.instr.getType() == 2){//update
			if(!node.suivants.isEmpty()){ //instruction is update instruction
				Invariant tmpInv = node.getInstr().update;

				node.suivants.getFirst().environ.listIne.addAll(tmpInv.listIne);
			}
			else System.out.println("fin de arbre");
		}
		System.out.println("VERIFIER UN NODE: "+YesNo+" !");
		return YesNo;
	}
	
	// executer affectation en utilisant post condition;mettre a jour aff.destination.environment
	public void executerAffectation(Node node, EnsembleVariable ev){
		Invariant tmpInv = postCondition(node.invariant,node.instr,ev);
		node.suivants.getFirst().environ = tmpInv;
		System.out.println("executerAffecatation");		
	}
	
	// verifier un arbre, un program en effet. en recurrence.
	public boolean verifierArbre(Node node, EnsembleVariable ev){
		boolean OuiNon = true;
		LinkedList<Node> visited = new LinkedList<Node>();
		visited.add(node);
		OuiNon = OuiNon & verifierNode(node,ev);
		if(node.suivants!=null){
			for(Node nodetmp : node.suivants){
	//			executerAffectation(nodetmp,ev);
				if(!visited.contains(nodetmp)){
					visited.add(nodetmp);
					OuiNon = OuiNon&verifierArbre(nodetmp,ev);
				}
			}
		}
		System.out.println("verifierArbre");		
		return OuiNon;
	}
	
	public static void main(String[] args) throws IOException {
//	/*	
	    String nomDeFichier = "ex1.txt";	
		EnsembleVariable ens = new EnsembleVariable(nomDeFichier);

		System.out.print(ens.size() + " VARIABLES:");
		for (int i = 0; i < ens.size(); i++) System.out.print(ens.getVariable(i).getNom()+",");
		System.out.println();
	    

		Block blc = new Block(nomDeFichier);blc.publish(blc.getmFirstNode(),ens);
	    
		Verificateur0 v0 = new Verificateur0();	
	    System.out.println("VOTRE PROGRAMME EST:"+v0.verifierArbre(blc.getmFirstNode(), ens));

	    blc.publish(blc.getmFirstNode(), ens);
//	 */ 
	}
}
